(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


Require Import Reals.
Open Scope R_scope.
Require Export Matrix.Mat.RMatrix.
Require Export Matrix.Mat.RMtacs.

(** Sg -> Ss *)

(* 侧滑角β (sidelip angle) *)
Parameter beta : R.

(* φ   *)
Parameter phi   : R.

(* μ   *)
Parameter my    : R.

(* γ  *)
Parameter gamma : R.


Definition coordinate_transform_SaSs : Mat R 3 3 := mkMat_3_3
  (cos beta) (-sin beta) 0
  (sin beta) (cos beta)  0
      0          0       1.

Definition coordinate_transform_SgSa : Mat R 3 3 := mkMat_3_3
  ((cos my)*(cos phi)) ((cos my)*(sin phi)) (-sin my)
  ((sin my)*(cos phi)*(sin gamma)-(sin phi)*(cos gamma))
  ((sin my)*(sin phi)*(sin gamma)+(cos phi)*(cos gamma))
  ((cos my)*(sin gamma))
  ((sin my)*(cos phi)*(cos gamma)+(sin phi)*(sin gamma))
  ((sin my)*(sin phi)*(cos gamma)-(cos phi)*(sin gamma)) 
  ((cos my)*(cos gamma)).


Definition SgToSs : Mat R 3 3 := mkMat_3_3
  ((cos beta)*(cos my)*(cos phi)+(-sin beta)*((sin my)*(cos phi)*(sin gamma)-(sin phi)*(cos gamma)))
  ((cos beta)*(cos my)*(sin phi)+(-sin beta)*((sin my)*(sin phi)*(sin gamma)+(cos phi)*(cos gamma)))
  ((cos beta)* (-sin my)+(-sin beta)*(cos my)*(sin gamma))
  ((sin beta)*(cos my)*(cos phi)+(cos beta)*((sin my)*(cos phi)*(sin gamma)-(sin phi)*(cos gamma)))
  ((sin beta)*(cos my)*(sin phi)+(cos beta)*((sin my)*(sin phi)*(sin gamma)+(cos phi)*(cos gamma)))
  ((sin beta)*(-sin my)+(cos beta)*(cos my)*(sin gamma))
  ((sin my)*(cos phi)*(cos gamma)+(sin phi)*(sin gamma)) 
  ((sin my)*(sin phi)*(cos gamma)-(cos phi)*(sin gamma)) ((cos my)*(cos gamma)).

Lemma SgToSs_eq :
  SgToSs === RMmul coordinate_transform_SaSs coordinate_transform_SgSa.
Proof.
  unfold SgToSs.
  RMat_mul_simpl. unfold mkMat_3_3'.
  f_equal2. ring. f_equal. ring. f_equal. ring. f_equal. ring. f_equal. ring.
  f_equal. ring. Qed. 
  


